YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { is_empty(nil()) -> true() , is_empty(cons(x, l)) -> false() , hd(cons(x, l)) -> x , tl(cons(x, l)) -> l , append(l1, l2) -> ifappend(l1, l2, l1) , ifappend(l1, l2, nil()) -> l2 , ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'custom shape polynomial interpretation' to orient following rules strictly. Trs: { is_empty(nil()) -> true() , is_empty(cons(x, l)) -> false() , hd(cons(x, l)) -> x , tl(cons(x, l)) -> l , append(l1, l2) -> ifappend(l1, l2, l1) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-restricted polynomial interpretation. [is_empty](x1) = 2 + x1 [nil]() = 0 [true]() = 0 [cons](x1, x2) = 1 + x1 + x2 [false]() = 1 [hd](x1) = 3 + 2*x1 [tl](x1) = 3 + 2*x1 [append](x1, x2) = 3 + 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2 + 3*x2^2 [ifappend](x1, x2, x3) = x1 + 3*x2 + 3*x2*x3 + 3*x2^2 + x3 + 3*x3^2 This order satisfies the following ordering constraints. [is_empty(nil())] = 2 > = [true()] [is_empty(cons(x, l))] = 3 + x + l > 1 = [false()] [hd(cons(x, l))] = 5 + 2*x + 2*l > x = [x] [tl(cons(x, l))] = 5 + 2*x + 2*l > l = [l] [append(l1, l2)] = 3 + 3*l1 + 3*l1*l2 + 3*l1^2 + 3*l2 + 3*l2^2 > 2*l1 + 3*l2 + 3*l2*l1 + 3*l2^2 + 3*l1^2 = [ifappend(l1, l2, l1)] [ifappend(l1, l2, nil())] = l1 + 3*l2 + 3*l2^2 >= l2 = [l2] [ifappend(l1, l2, cons(x, l))] = l1 + 6*l2 + 3*l2*x + 3*l2*l + 3*l2^2 + 4 + 7*x + 7*l + 3*x^2 + 3*x*l + 3*l*x + 3*l^2 >= 4 + x + 3*l + 3*l*l2 + 3*l^2 + 3*l2 + 3*l2^2 = [cons(x, append(l, l2))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { ifappend(l1, l2, nil()) -> l2 , ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) } Weak Trs: { is_empty(nil()) -> true() , is_empty(cons(x, l)) -> false() , hd(cons(x, l)) -> x , tl(cons(x, l)) -> l , append(l1, l2) -> ifappend(l1, l2, l1) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'custom shape polynomial interpretation' to orient following rules strictly. Trs: { ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-restricted polynomial interpretation. [is_empty](x1) = 2 + x1 [nil]() = 0 [true]() = 0 [cons](x1, x2) = 1 + x1 + x2 [false]() = 1 [hd](x1) = 3 + x1 [tl](x1) = 3 + 2*x1 [append](x1, x2) = 3*x1 + 3*x1*x2 + 2*x1^2 + 3*x2 + 3*x2^2 [ifappend](x1, x2, x3) = x1 + 3*x2 + 3*x2*x3 + 3*x2^2 + 2*x3 + 2*x3^2 This order satisfies the following ordering constraints. [is_empty(nil())] = 2 > = [true()] [is_empty(cons(x, l))] = 3 + x + l > 1 = [false()] [hd(cons(x, l))] = 4 + x + l > x = [x] [tl(cons(x, l))] = 5 + 2*x + 2*l > l = [l] [append(l1, l2)] = 3*l1 + 3*l1*l2 + 2*l1^2 + 3*l2 + 3*l2^2 >= 3*l1 + 3*l2 + 3*l2*l1 + 3*l2^2 + 2*l1^2 = [ifappend(l1, l2, l1)] [ifappend(l1, l2, nil())] = l1 + 3*l2 + 3*l2^2 >= l2 = [l2] [ifappend(l1, l2, cons(x, l))] = l1 + 6*l2 + 3*l2*x + 3*l2*l + 3*l2^2 + 4 + 6*x + 6*l + 2*x^2 + 2*x*l + 2*l*x + 2*l^2 > 1 + x + 3*l + 3*l*l2 + 2*l^2 + 3*l2 + 3*l2^2 = [cons(x, append(l, l2))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { ifappend(l1, l2, nil()) -> l2 } Weak Trs: { is_empty(nil()) -> true() , is_empty(cons(x, l)) -> false() , hd(cons(x, l)) -> x , tl(cons(x, l)) -> l , append(l1, l2) -> ifappend(l1, l2, l1) , ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'custom shape polynomial interpretation' to orient following rules strictly. Trs: { ifappend(l1, l2, nil()) -> l2 } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^2)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-restricted polynomial interpretation. [is_empty](x1) = 2 + x1 [nil]() = 0 [true]() = 0 [cons](x1, x2) = 1 + x1 + x2 [false]() = 1 [hd](x1) = 3 + x1 [tl](x1) = 3 + x1 [append](x1, x2) = 3 + 3*x1 + 3*x1*x2 + x1^2 + 3*x2 + 3*x2^2 [ifappend](x1, x2, x3) = 2 + x1 + 3*x2 + 3*x2*x3 + 3*x2^2 + 2*x3 + x3^2 This order satisfies the following ordering constraints. [is_empty(nil())] = 2 > = [true()] [is_empty(cons(x, l))] = 3 + x + l > 1 = [false()] [hd(cons(x, l))] = 4 + x + l > x = [x] [tl(cons(x, l))] = 4 + x + l > l = [l] [append(l1, l2)] = 3 + 3*l1 + 3*l1*l2 + l1^2 + 3*l2 + 3*l2^2 > 2 + 3*l1 + 3*l2 + 3*l2*l1 + 3*l2^2 + l1^2 = [ifappend(l1, l2, l1)] [ifappend(l1, l2, nil())] = 2 + l1 + 3*l2 + 3*l2^2 > l2 = [l2] [ifappend(l1, l2, cons(x, l))] = 5 + l1 + 6*l2 + 3*l2*x + 3*l2*l + 3*l2^2 + 4*x + 4*l + x^2 + x*l + l*x + l^2 > 4 + x + 3*l + 3*l*l2 + l^2 + 3*l2 + 3*l2^2 = [cons(x, append(l, l2))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { is_empty(nil()) -> true() , is_empty(cons(x, l)) -> false() , hd(cons(x, l)) -> x , tl(cons(x, l)) -> l , append(l1, l2) -> ifappend(l1, l2, l1) , ifappend(l1, l2, nil()) -> l2 , ifappend(l1, l2, cons(x, l)) -> cons(x, append(l, l2)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))